/**
 * 
 */
package extensionTools.smvCreator;

import java.util.ArrayList;
import java.util.Dictionary;
import java.util.Enumeration;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
import java.util.Set;

import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;
import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;

/**
 * This class  holds static functions which are needed
 * in several rules classes
 * @author dani
 *
 */
public class RulesUtils 
{
     public static class Assoc
     {
             private String assocString;
             private String srcName;
             private long srcId;
             private String dstName;
             private long dstId;
             private SmvProcess process; //father_to_leaf proc
             private State srcState;
             private State dstState;
             
             
             /**
              * Assoc present the variable assoc_proc_obj / assoc_obj_obj
              * @param assocString
              * @param srcName
              * @param dstName
              * @param process
              */
             Assoc(String assocString, String srcName, String dstName, long srcId, long dstId, State srcState,  State dstState, SmvProcess process)
             {
                     this.assocString = assocString;
                     this.srcName = srcName;
                     this.srcId = srcId;
                     this.dstName = dstName;
                     this.dstId = dstId;
                     this.srcState = srcState;
                     this.dstState = dstState;
                     this.process = process;
             }

            public String getAssocString() {
                    return assocString;
            }

            public String getSrcName() {
                    return srcName;
            }

            public String getDstName() {
                    return dstName;
            }

            public SmvProcess getProcess() {
                    return process;
            }

			public void setSrcId(long srcId) {
				this.srcId = srcId;
			}

			public long getSrcId() {
				return srcId;
			}

			public void setDstId(long dstId) {
				this.dstId = dstId;
			}

			public long getDstId() {
				return dstId;
			}

			public void setSrcState(State srcState) {
				this.srcState = srcState;
			}

			public State getSrcState() {
				return srcState;
			}

			public void setDstState(State dstState) {
				this.dstState = dstState;
			}

			public State getDstState() {
				return dstState;
			}
		
     }
     
     public static class ObjectAndRelatedState
     {
    	 private SmvObject object;
    	 private State state;
    	 
    	 ObjectAndRelatedState(SmvObject object, State state)
    	 {
    		this.setObject(object);
    		this.setState(state);
    	 }

		public void setObject(SmvObject object) {
			this.object = object;
		}

		public SmvObject getObject() {
			return object;
		}

		public void setState(State state) {
			this.state = state;
		}

		public State getState() {
			return state;
		}
     }
 
    static public ArrayList<Assoc> assocProcObj = new ArrayList<Assoc>();
    static public ArrayList<Assoc> assocObjObj= new ArrayList<Assoc>();

    /**
     * This function create ArrayList<Assoc> assocProcObj and ArrayList<Assoc> assocObjObj
     * @param db
     * @param currProc
     * @return ArrayList<ArrayList<Assoc>>: 
     * 		   ArrayList<ArrayList<Assoc>>[0] = ArrayList<Assoc> assocProcObj
     * 		   ArrayList<ArrayList<Assoc>>[1] = ArrayList<Assoc> assocObjObj
     */
    public static ArrayList<ArrayList<Assoc>> creatAssocsList(DiagramDatabase db, SmvProcess currProc) 
    {   
         
	     //relatedObjectDictionary holds all the objects that are connected to the child's process.
	     Dictionary<Long, ObjectAndRelatedState> relatedObjectDictionary = new Hashtable<Long, ObjectAndRelatedState>();
	     
	     for(SmvProcess currChild : db.getChildrenList(currProc))
	     {
	         ArrayList<ObjectAndRelatedState> relatedObjectsWithResultTocurrChild = processHaveResultLink(db, currChild, relatedObjectDictionary);
	                 
	         for(int i=0; i<relatedObjectsWithResultTocurrChild.size();i++)
	         { 
	             //Handle assoc_proc_obj (src=process, dst=object)
	        	 //null is for srcState - process desn't have states!
	             assocProcObj = createAssocVars(currProc.getName(), relatedObjectsWithResultTocurrChild.get(i).getObject().getName(), 
	            		                        currProc.getId(), relatedObjectsWithResultTocurrChild.get(i).getObject().getId(), 
	            		                        null, relatedObjectsWithResultTocurrChild.get(i).getState(), currProc, assocProcObj);                              
	         }   
	         
	         ArrayList<ObjectAndRelatedState> relatedObjectsWithConsumptionTocurrChild = processHaveConsumptionLink(db, currChild, relatedObjectDictionary);
	           
	         for(int i=0; i<relatedObjectsWithConsumptionTocurrChild.size();i++)
	         { 
	             //Handle assoc_proc_obj (src=object, dst=process)
	        	 //null is for dstState - process desn't have states!
	             assocProcObj = createAssocVars(relatedObjectsWithConsumptionTocurrChild.get(i).getObject().getName(), currProc.getName(),
	            		                        relatedObjectsWithConsumptionTocurrChild.get(i).getObject().getId(), currProc.getId(), 
	            		                        relatedObjectsWithConsumptionTocurrChild.get(i).getState(), null, currProc, assocProcObj);                              
	         }   
	     }                                                       
         
         //create list of all assoc_obj_obj variables with structural links
	     Enumeration<ObjectAndRelatedState> objectsWithStates = relatedObjectDictionary.elements();      
	     //Enumeration<SmvObject> relatedObjects =  relatedObjectDictionary.elements();                 
         while(objectsWithStates!=null && objectsWithStates.hasMoreElements())
         {
             ObjectAndRelatedState currObjectWithState = objectsWithStates.nextElement();            
             SmvObject currObject = currObjectWithState.getObject();
                          
             for(Link currLink : currObject.getLinkList())
             {                             
                 if ( (currLink.getLinkType() == LinkType.CHARACTERIZATION || 
                       currLink.getLinkType() == LinkType.PARTICULATION  || 
                       currLink.getLinkType() == LinkType.UNIDIRECTIONAL ||
                       currLink.getLinkType() == LinkType.BIDIRECTIONAL) &&
                       (relatedObjectDictionary.get(currLink.getDstId())!=null) && //to make sure that both edge objects connected to currProc 
                       (currLink.getSrcId() == currObject.getId())) //to prevent duplicates
                    {
                         String objDestName = RulesUtils.getLinkEdgeName(currLink, db, false);
                         
                         //dest object has state
                         if(currLink.getDstType() == SmvType.STATE)
                         {
                        	 State dstState = db.getSmvStateList().get(db.findStateById(currLink.getDstId()));
                        	 
                        	 assocObjObj = createAssocVars(relatedObjectDictionary.get(currLink.getSrcId()).getObject().getName(), objDestName, 
      		 					   relatedObjectDictionary.get(currLink.getSrcId()).getObject().getId(), currLink.getDstId(),
      		 					   relatedObjectDictionary.get(currLink.getSrcId()).getState(), dstState, currProc, assocObjObj);
                         }
                         else //dest object doesn't has state
                         {
                        	 assocObjObj = createAssocVars(relatedObjectDictionary.get(currLink.getSrcId()).getObject().getName(), objDestName, 
                        		 					   relatedObjectDictionary.get(currLink.getSrcId()).getObject().getId(), currLink.getDstId(),
                        		 					   relatedObjectDictionary.get(currLink.getSrcId()).getState(), null, currProc, assocObjObj);
                         }
                    }    
             }                              
         }
         
         ArrayList<ArrayList<Assoc>> retVal = new ArrayList<ArrayList<Assoc>>();
         retVal.add(assocProcObj);
         retVal.add(assocObjObj);
         
         return retVal;
    }

    /**
     * This function return the AssocString from assocProcObj List that belong to given objName+procName
     * @param objName
     * @param procName
     * @return assocString
     */
     public static String findAssoc(String objName, String procName) 
     {
         for(Assoc currProcObj : assocProcObj)
         {
             if(((currProcObj.getSrcName().equals(procName)) && (currProcObj.getDstName().equals(objName))) ||
                ((currProcObj.getDstName().equals(procName)) && (currProcObj.getSrcName().equals(objName))))
             {
                 return currProcObj.getAssocString();
             }
         }
         return "";
     }
     
     /**
      * This function create new ASSOC and add it to ArrayList<Assoc> AssocVars
      * @param srcName
      * @param dstName
      * @param currProc
      * @param AssocVars
      * @return
      */
     public static ArrayList<Assoc> createAssocVars(String srcName, String dstName, long srcId, long dstId, State srcState, State dstState, SmvProcess currProc, ArrayList<Assoc> AssocVars) 
     {
             for(int i=0;i<SMVCreator.K;i++)
             {
                      for (int j=0;j<SMVCreator.K;j++)
                      {
                          AssocVars.add(new Assoc("assoc_"+srcName+"_"+j+"_"+dstName+"_"+i, srcName+"_"+j, dstName+"_"+i, srcId, dstId, srcState, dstState, currProc));
                      }      
             }
             return AssocVars;
     }
     
     /**
      * This function find all objects that connected in consumption link to the given process.
      * @param currChild a SmvProcess
      * @return
      */
     public static ArrayList<ObjectAndRelatedState> processHaveConsumptionLink(DiagramDatabase db, SmvProcess currChild, Dictionary<Long, ObjectAndRelatedState> relatedObjectList) 
     {
    	 ArrayList<ObjectAndRelatedState> relatedObjectListToCurrChild = new ArrayList<ObjectAndRelatedState>(); 
         
    	//get all objects related to the children of the process with result link
         for(Link currLink : currChild.getLinkList())
         {
	    	 if(currLink.getLinkType() == LinkType.CONSUMPTION)
			 {
	  			if(currLink.getSrcType() == SmvType.STATE)
	             {
	                 State relatedState = db.getSmvStateList().get(db.findStateById(currLink.getSrcId()));
	                 SmvObject object = db.getSmvObjectList().get(db.findObjectById(relatedState.getObjectId()));
	                 
	                 ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, relatedState);
	                 
	                 relatedObjectListToCurrChild.add(objectWithState);
	                 relatedObjectList.put(object.getId(), objectWithState);
	             }
	             else //currLink.getSrcType() == SmvType.OBJECT
	             {
	                 SmvObject object = db.getSmvObjectList().get(db.findObjectById(currLink.getSrcId()));
	                 
	                 ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, null);
	                 
	                 relatedObjectListToCurrChild.add(objectWithState);
	                 relatedObjectList.put(object.getId(), objectWithState);
	             }
	  		}
         }
         
         return relatedObjectListToCurrChild;
     }
     
     
     /**
     * This function find all objects that connected in result link to the given process.
     * @param currChild a SmvProcess
     * @return
     */
     static public ArrayList<ObjectAndRelatedState> processHaveResultLink(DiagramDatabase db, SmvProcess currChild, Dictionary<Long, ObjectAndRelatedState> relatedObjectList) 
     {
         ArrayList<ObjectAndRelatedState> relatedObjectListToCurrChild = new ArrayList<ObjectAndRelatedState>(); 
         
         //get all objects related to the children of the process with result link
         for(Link currLink : currChild.getLinkList())
         {
             if(currLink.getLinkType() == LinkType.RESULT)
             {
                 if(currLink.getDstType() == SmvType.STATE)
                 {
                     State relatedState = db.getSmvStateList().get(db.findStateById(currLink.getDstId()));
                     SmvObject object = db.getSmvObjectList().get(db.findObjectById(relatedState.getObjectId()));
                     
                     ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, relatedState);
                     
                     relatedObjectListToCurrChild.add(objectWithState);
                     relatedObjectList.put(object.getId(), objectWithState);
                 }
                 else //currLink.getDstType() == SmvType.OBJECT
                 {
                     SmvObject object = db.getSmvObjectList().get(db.findObjectById(currLink.getDstId()));
                     
                     ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, null);
                     
                     relatedObjectListToCurrChild.add(objectWithState);
                     relatedObjectList.put(object.getId(), objectWithState);
                 }
             }
    		
         }
             
        //get all objects related to the children of the process with or link
        ArrayList<ArrayList<Link>> orLists = new ArrayList<ArrayList<Link>>();
        orLists = currChild.getOrLists();
        
        if(orLists.size() != 0)
        {
        	for(int i = 0; i < orLists.size(); i++)
        	{
        		for(Link currOrLink : orLists.get(i))
        		{
        			if(currOrLink.getLinkType() == LinkType.RESULT && currOrLink.getSrcType() == SmvType.PROCESS)
                    {
                        if(currOrLink.getDstType() == SmvType.STATE)
                        {
                            State relatedState = db.getSmvStateList().get(db.findStateById(currOrLink.getDstId()));
                            SmvObject object = db.getSmvObjectList().get(db.findObjectById(relatedState.getObjectId()));                           
                            ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, relatedState);
                                                       
                            relatedObjectListToCurrChild.add(objectWithState);
                            relatedObjectList.put(object.getId(), objectWithState);
                        }
                        else //currLink.getDstType() == SmvType.OBJECT
                        {
                            SmvObject object = db.getSmvObjectList().get(db.findObjectById(currOrLink.getDstId()));
                            ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, null);
                            
                            relatedObjectListToCurrChild.add(objectWithState);
                            relatedObjectList.put(object.getId(), objectWithState);
                        }
                    }
        		}
        	}
        }
        	
    	//get all objects related to the children of the process with xor link
        ArrayList<ArrayList<Link>> xorLists= new ArrayList<ArrayList<Link>>();
        xorLists = currChild.getXorLists();
       
        if(xorLists.size() != 0)
        {
        	for(int i = 0; i < xorLists.size(); i++)
        	{
        		for(Link currXorLink : xorLists.get(i))
        		{
        			if(currXorLink.getLinkType() == LinkType.RESULT && currXorLink.getSrcType() == SmvType.PROCESS)
                    {
                        if(currXorLink.getDstType() == SmvType.STATE)
                        {
                            State relatedState = db.getSmvStateList().get(db.findStateById(currXorLink.getDstId()));
                            SmvObject object = db.getSmvObjectList().get(db.findObjectById(relatedState.getObjectId()));
                            
                            ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object, relatedState);
                            
                            relatedObjectListToCurrChild.add(objectWithState);
                            relatedObjectList.put(object.getId(), objectWithState);
                        }
                        else //currLink.getDstType() == SmvType.OBJECT
                        {
                            SmvObject object = db.getSmvObjectList().get(db.findObjectById(currXorLink.getDstId()));
                            
                            ObjectAndRelatedState objectWithState = new ObjectAndRelatedState(object,null);                           
                            
                            relatedObjectListToCurrChild.add(objectWithState);
                            relatedObjectList.put(object.getId(), objectWithState);
                        }
                    }
        		}
        	}
        }
        
        return relatedObjectListToCurrChild;
     }
    
        /**
     * This function gets a process's ID and returns the process from the DB if 
         * he's there, null otherwise 
         * @param srcId
         * @return the process which this procId belongs to
         */
    public static SmvProcess getProccessbyId(long procId,DiagramDatabase db) 
    {      
            int plc = db.findProcessById(procId);
            if (-1 == plc)
                    return null;
            return db.getSmvProcessList().get(plc);
    }

    /**
     * This function gets an object's ID and returns the object from the DB if 
     * he's there, null otherwise 
     * @param srcId
     * @return the object which this objId belongs to
     */
    public static SmvObject getObjectbyId(long objId,DiagramDatabase db) 
    {  
            int plc = db.findObjectById(objId);
            if (-1 == plc)
                    return null;
            return db.getSmvObjectList().get(plc);
    }
        
    
        /**
         * 
         * @param obj
         * @return the names of the states the object has with comma between them.
         */
        public static String getStateNames(SmvObject obj) {
                ArrayList<State> states = obj.getStateList();
                String stateNames = "";
                if(states == null || 0 == states.size()) 
                        stateNames = "exist,";
                else
                        for (State state : states) {
                                stateNames += state.getName() +",";
                        }
                return stateNames + "notExist";
        }
        
        /**
         * This function gets a link and return it's 
         * edge's name (either src or dst)
         * @param link - the link we're interested in
         * @param db - the current diagram database
         * @param srcFlag - if true we want src, dst otherwise
         * @return a string containing the src name (object or process)
         */
        public static String getLinkEdgeName(Link link, DiagramDatabase db, boolean srcFlag){
                if (link == null || db == null) return null;
                String srcName = null;
                SmvType edgeType;
                long edgeId;
                if(srcFlag){
                        edgeType = link.getSrcType();
                        edgeId = link.getSrcId();
                }
                else{ 
                        edgeType = link.getDstType();
                        edgeId = link.getDstId();
                }
                switch (edgeType){
                case OBJECT:
                        SmvObject obj = getObjectbyId(edgeId, db);
                        if(obj!=null) srcName = obj.getName();
                        else{
                                SmvInstanceObject instobj = getObjectInstanceById(edgeId,db);
                                if(instobj!=null) srcName = instobj.getFatherInstanceName();    
                        }
                        break;
                case PROCESS:
                        SmvProcess proc = getProccessbyId(edgeId, db); 
                        if(proc!=null) srcName = proc.getName();
                        break;
                // if we got a state, we would return the object he belongs to
                case STATE:
                        State state = getStatebyId(db.findStateById(edgeId),db);
                        if(state == null) break;
                        SmvObject obj2 = getObjectbyId(state.getObjectId(),db);
                        if(obj2 != null) srcName = obj2.getName();
                        break;
                }
                return srcName;
        }
        
        /**
         * 
         * @param edgeId
         * @param db the diagram database
         * @return
         */
        public static SmvInstanceObject getObjectInstanceById(long edgeId,
                                DiagramDatabase db) {
            int plc = db.findInstanceObjectById(edgeId);
            if (-1 == plc)
                    return null;
            return db.getSmvInstanceObjectList().get(plc);
        }

                /**
         * Given an SMV process, this functions finds one of its predecessor timeline-wise.
         * If the given process is not the first one in the timeline of the father procees,
         * it returns one of the process above it. Otherwise, it returns the father.
         * @param proc an SMV process
         * @return the previous SMV process in the timeline
                 * @throws RulesUtilsException 
         */
        public static SmvProcess getPrevProcessId(SmvProcess proc, DiagramDatabase db) throws RulesUtilsException{
                long procFatherId = proc.getFatherId();
                //int procFatherIndex = db.findProcessById(procFatherId);               
                //SmvProcess procFather = db.getSmvProcessList().get(procFatherIndex);
                
                SmvProcess procFather = getProccessbyId(procFatherId, db);
                //if the process is the first in the timeline, the previous process in its father process
                if (proc.getTimeLine() == 1) {
                        return procFather;
                }
                //otherwise, there is a process above it in the timeline
                else {
                        for (long childId : procFather.getChildrenIdList()) {
                                int childIndex = db.findProcessById(childId);
                                SmvProcess child = db.getSmvProcessList().get(childIndex);
                                if (child.getTimeLine() == (proc.getTimeLine()-1)) {
                                        return child;
                                }
                        }
                }
                throw new RulesUtilsException("RulesUtils: The given process" + proc.getName() +
                								"doesn't have a prev process");
        }
        
        /**
         * 
         * @param proc
         * @param db
         * @return
         */
        public static ArrayList<String> getAllAncestorProcs(SmvProcess proc, DiagramDatabase db) {
     	   ArrayList<String> ancestors = new ArrayList<String>();
     	   
     	   SmvProcess currProc = proc;
     	   while (currProc.getFatherId() != -1 ) {
     		   SmvProcess father = RulesUtils.getProccessbyId(currProc.getFatherId(), db);
     		   if (! father.equals(proc)) {
 	    		   ancestors.add(father.getName());
 	    		   currProc = father;
     		   }
     	   }
     	   return ancestors;
        }
        
        /**
         * @param proc an SMV process
         * @param db 
         * @return an ArrayList of all the SMV processes which have the same father id
         * as proc, and are located at the same time line as proc
         */
       public static HashSet<String> getProcsInSameTimeline(SmvProcess proc, DiagramDatabase db){
           HashSet<String> procs = new HashSet<String>();
        
                for (SmvProcess currProc : db.getSmvProcessList()) {
                        if ((currProc.getFatherId() == proc.getFatherId()) && 
                           (currProc.getTimeLine() == proc.getTimeLine()))
                        {  
                        	procs.add(currProc.getName());
                        }
                }
                return procs;
        }
       
       /**
        * 
        * @param procs hash set of process names
        * @param i the current instance
        * @param waitForState
        * @param db
        * @return
        * @throws RulesUtilsException
        */
       public static ArrayList<String> createWaitProcessCondition(HashSet<String> procs, int i, 
					String waitForState, DiagramDatabase db ) throws RulesUtilsException
		{
    	   ArrayList<String> results = new ArrayList<String>();
    	   String tempRes = "";
    	   String condition = "";
    	   Object[] procArray = procs.toArray();
		
    	   if (procs.size() < 1) {
    		   
    		   return results;
    	   }
    	   //If the process if the first in the timeline
    	   if ( (procs.size() == 1) && (waitForState.equals("active")) ) {
    		  tempRes = procArray[0] + "_" + i + " = " + waitForState; 
    		  results.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", tempRes), "TRUE"));
    	   }
    	   else {
	    	   int[] vector = new int[procs.size()]; 
	           for (int j=0; j < vector.length; j++) {
	                   vector[j] = 0;
	           }           
	           while (vector != null) {
	                   int j=0;
	                   for (String currProc : procs){                       
	                       if (vector[j]  == 0) {
	                    	   condition = currProc + "_" + i + " = " + waitForState;
	                       }
	                       else {
	                    	   condition = "ev_terminate_" + currProc + "_" + i + " = 0";
	                       }
	                	  
	                	   tempRes = SmvOp.and(condition, tempRes);
	                       j++;
	                   }
	                   results.add(SmvOp.createCaseLine(SmvOp.and("sysState = event1", tempRes), "TRUE"));
	                   vector = getNextVector(vector, 2);
	                   tempRes = "";
	           }
    	   }
		
    	   return results;   
		}
        
        /*
        public static ArrayList<String> getEvXorCombinations(String procName, ArrayList<String> objs) {
                //TODO: luba - don't send K, you can get it when you call SMVCreator.K because it's global variable
                ArrayList<String> result = new ArrayList<String>();
                String tempRes = "";
                String lastDash = "";
                int[] vector = new int[objs.size()+1]; 
                for (int i=0; i < vector.length; i++) {
                        vector[i] = 0;
                }
                
                while (vector != null) {
                        tempRes = "ev_xor_" + procName + "_"+ Integer.toString(vector[0]) + "_";
                        int i=1;
                        for (String objName : objs){
                                if (objName.equals(objs.get(objs.size()-1))){
                                        lastDash = "";
                                }
                                else {
                                        lastDash = "_";
                                }
                                tempRes = tempRes + objName + "_" + Integer.toString(vector[i]) + lastDash;
                                i++;
                        }
                        result.add(tempRes);
                        vector = getNextVector(vector, SMVCreator.K);
                }
                return result;
        }
        */
        



       /**
        * @param an array of integers representing a number in base k
        * @param k base
        * @return a vector in base k representing the next number in k base
        */
       public static int[] getNextVector(int[] vector, int k) {
    	   vector[0]++;
           for (int i=0; i < vector.length ; i++ ) {
        	   if (vector[i] == k) {
        		   if (i == vector.length - 1) {
        			   return null;
                   }
                   vector[i] = 0;
                   if (i+1 < vector.length) {
                	   vector[i+1]++;
                   }
               }
           }
           return vector;
        }

             
                
        
        /**
         * The method returns all subsets of a given ArrayList<String>
         * @param set
         * @return all subsets of set
         */
       
        private static ArrayList<ArrayList<String>> getSubsets( ArrayList<String> set) {

    		ArrayList<ArrayList<String>> subsetCollection = new ArrayList<ArrayList<String>>();

    		if (set.size() == 0) {
    			subsetCollection.add(new ArrayList<String>());
    		} else {
    			ArrayList<String> reducedSet = new ArrayList<String>();

    			reducedSet.addAll(set);

    			String first = reducedSet.remove(0);
    			ArrayList<ArrayList<String>> subsets = getSubsets(reducedSet);
    			subsetCollection.addAll(subsets);

    			subsets = getSubsets(reducedSet);

    			for (ArrayList<String> subset : subsets) {
    				subset.add(0, first);
    			}

    			subsetCollection.addAll(subsets);
    		}

    		return subsetCollection;
    	}
        
        /**
         * This function gets db and index location, and returns the state from
         * the db's states arrayList
         * @param index
         * @param db
         * @return the state if found, null otherwise (some error occurred 
         */
        public static State getStatebyId(int index,DiagramDatabase db) {
                if (-1 == index)
                        return null;
                return db.getSmvStateList().get(index);
        }
        
        /**
         * This function gets and ArrayList<String> and returns a matching array
         * @param rules - usually the case lines
         * @return arr - a matching array
         * @throws RulesUtilsException - when there was an error trying to convert ArrayList to array
         */
                public static String[] arrayListToArray(ArrayList<String> rules) throws RulesUtilsException {
                        if(rules == null) return null;
                        int size = rules.size(),i=0;
                        String[] arr = new String[size];
                        for (String line : rules) {
                                if(i>=size) throw new RulesUtilsException("RulesUtils: Something not right with ArrayList sent");
                                arr[i]= line;
                                i++;
                        }       
                        return arr;
                }
        /**
         * This function concatenate two strings arrays into one
         * @return A new array that is the concatenation of the to arrays that where
         * given as parameters, or return the parameter array if the other was null
         */
                public static String[] combineStrings(String[] stringArr1,
                                String[] stringArr2) {


                        if (stringArr1 == null)
                        {
                                return stringArr2;
                        }
                        if (stringArr2 == null)
                        {
                                return stringArr1;
                        }
                        String[] newStringArr = new String[stringArr1.length+stringArr2.length];

                        int j=0;
                        for (;j<stringArr1.length;j++)
                        {
                                newStringArr[j]=stringArr1[j];
                        }
                        for (int i=0;i<stringArr2.length;i++)
                        {
                                newStringArr[i+j]=stringArr2[i];
                        }
                        return newStringArr;
                }
                
                /**
                 * convert string[] to string.
                 * @param stringArr
                 * @return
                 */
                public static String stringArrayToString(String[] stringArr)
                {
                	if (stringArr == null) return "";
                	String res = "";
                	for(int i=0;i<stringArr.length;i++)
                	{
                		res+=stringArr[i];
                	}
                	
                	return res;
                }      
        /**
         * This function adds a default rule line in the end of the rules array
         * @param CaseLines - the String array that holds all the lines of a rule
         * @param result - the default rule line to add
         * @param caseVar -the case in the rule
         * @return A new array that is the concatenation of the rules array
         * and the default rule line
         * @throws RulesUtilsException - when null parameters were sent to SmvOp
         */
        public static String[] addDefaultState(String[] CaseLines,
                                String caseVar, String result) throws RulesUtilsException {

                String[] newCaseLine = new String[1];
                newCaseLine[0] = SmvOp.createCaseLine(caseVar , result);
                return combineStrings(CaseLines,newCaseLine);
                        
                }
        
        
        /**
         * This function creates a power set of a given set
         * @param originalSet - the original set
         * @return A power set og the originalSet set
         */
        
        public static <T> Set<Set<T>> powerSet(Set<T> originalSet) {
            Set<Set<T>> sets = new HashSet<Set<T>>();
            if (originalSet.isEmpty()) {
                sets.add(new HashSet<T>());
                return sets;
            }
            List<T> list = new ArrayList<T>(originalSet);
            T head = list.get(0);
            Set<T> rest = new HashSet<T>(list.subList(1, list.size())); 
            for (Set<T> set : powerSet(rest)) {
                Set<T> newSet = new HashSet<T>();
                newSet.add(head);
                newSet.addAll(set);
                sets.add(newSet);
                sets.add(set);
            }           
            return sets;
        }
        
        /**
         * This function creates a String containing all Object named currObjName name
         * instances. Example:
         * @param currObjName 
         * @param instancesSet - set of instances numbers
         * @return A Set of Strings containing currObjName_i 
         */
        public static Set<String> nameAllObjectInstances(String currObjName,
        		Set<Integer> instanceSet) {
    	
    		Set<String> nameSet = new HashSet<String>();
    		for (Integer i:instanceSet)
    		{
    			nameSet.add(currObjName+"_"+i);
    		}
    	return nameSet;
    }
        /**
         * This function sorts the List by string length
         * @param list - list to sort 
         */
		public static void sortBySize(ArrayList<String> list) 
		{
			int top = list.size();
			for (int i = 0;i < top; ++i)
			{
				for (int j = 1; j < top; ++j)
				{
					String a = list.get(j-1);
					String b = list.get(j);
					if (a.length() < b.length())
					{
						list.set(j-1, b);
						list.set(j, a);
					}
				}
			}
		}
		
        /**
         * This function return the difference between two sets (bigSet\s)
         * @param bigSet - main Set
         * @param s
         * @return The difference set
         * @throws RulesUtilsException - if one of the parameters is null
         */		
		@SuppressWarnings("unchecked")
		public static <T> Set<T> diffrenceSet(Set<T> bigSet, Set<T> s) throws RulesUtilsException 
		{
			if (bigSet == null || s == null)
			{
				checkParamsForNull(bigSet,s);
			}
			Set<T> diffSet = new HashSet<T>(bigSet);;
			for (T num: s)
			{
				diffSet.remove(num);
			}
			return diffSet;
		}
		
        /**
         * This function check if one of the parameters sent to her is a null parameter
         * @param bigSet 
         * @param s
         * @return The difference set
         */	
		public static <T> void checkParamsForNull(T... params)throws RulesUtilsException
		{
			int i=0;
			for (T param : params)
			{
				i++;
				if (param == null)
				{
					throw new RulesUtilsException("RulesUtils: The "+i+"rd parameter is a null parameter");
				}
			}
			return;
		}

	/**
	 * This function gets ArrayLink full of links, and returns their names in ArrayList
	 * @param or - the arraylist of links
	 * @return the names of the destinations, if all are objects
	 * @throws SmvDBException - in case of invalid destination
	 */
	static public ArrayList<String> getDstNames(ArrayList<Link> or, DiagramDatabase db) throws SmvDBException {
		ArrayList<String> names = new ArrayList<String>();
		for (Link link : or) {
			switch (link.getDstType() ){
			case OBJECT:
			case STATE:
				names.add(RulesUtils.getLinkEdgeName(link, db, false));
				break;
			default:
				throw new SmvDBException("RulesUtils: unexpected edge type in link from "+link.getSrcType());
			}
		}
		return names;
	}
	
	/* Xor/Or related methods */
	
	/**
     * Check if a given Link is a XOR link
     * @param DiagramDatabase, Link
     * @return return all the links in the xor connection with a given link
     * @throws RulesUtilsException - when recieving null parameters
     */
    public static ArrayList<Link> lnkInXor(DiagramDatabase db, Link lnk) throws RulesUtilsException {
            
        if (null == db || null == lnk)
        {
        	throw new RulesUtilsException("RulesUtils: got null parameters where link and DB expecter in lnkInOr");
        }
                for (ArrayList<Link> currXorList: db.getSmvProcessList().
                                get(db.findProcessById(lnk.getSrcId())).getXorLists()) {
                        for (Link currLink: currXorList)
                        {
                                if (currLink.getDstId() == lnk.getDstId() && 
                                                currLink.getSrcId() == lnk.getSrcId())
                                {
                                        return currXorList;
                                }
                        }
        }
            return null;
    }
        /**
         * Check if a given Link is a OR link
         * @param DiagramDatabase, Link
         * @return return all the links in the or connection with a given link
         * @throws RulesUtilsException - when recieving null parameters
         */
        public static ArrayList<Link> lnkInOr(DiagramDatabase db, Link lnk) throws RulesUtilsException {
                
                if (null == db || null == lnk)
                {
                        throw new RulesUtilsException("RulesUtils: got null parameters where link and DB expecter in lnkInOr");
                }
                        for (ArrayList<Link> currOrList: db.getSmvProcessList().
                                        get(db.findProcessById(lnk.getSrcId())).getOrLists()) {
                                for (Link currLink: currOrList)
                                {
                                        if (currLink.getDstId() == lnk.getDstId() && 
                                                        currLink.getSrcId() == lnk.getSrcId())
                                        {
                                                return currOrList;
                                        }
                                }
                }
                return null;
        }
        
        /**
         * This function returns the names of the xor/or variable as the keys
         * and their possible states as a string state1,state2,state1state2,...
         * according to the objects list and the type of relation 
         * @param procName - the process name
         * @param objs - a list of objects names 
         * @return a dictionary with var names as keys and possible values as value
         * @throws RulesUtilsException 
         */
        public static Dictionary<String, String> getXorDict(String procName, ArrayList<String> objs,boolean xorFlag) throws RulesUtilsException{
                Dictionary<String, String> xorDict = new Hashtable<String, String>();
                if(objs == null || objs.size() < 2){
                        throw new RulesUtilsException("RulesUtils: Not enough objecs sent to xor function at "+procName);
                }
                //proc instantiations
                for (int i=0; i<SMVCreator.K;i++){
                        String linkName = (xorFlag)? "ev_xor_" : "ev_or_";
                    linkName+= procName+"_"+i+"_";
                        ArrayList<String> enumer = new ArrayList<String>();
                        fillUpDict(xorDict,linkName,enumer,objs,xorFlag);
                }
                return xorDict;
        }
        
        /**
         * This function returns dictionary of the xor/or variable as the keys
         * and their possible instances of every object int the key name as an array 
         * for example ev_xor_proc1_0_obj1_0_obj2_1=[0,1]
         * according to the objects list and the type of relation 
         * @param procName - the process name
         * @param objs - a list of objects names 
         * @return a dictionary with var names as keys and possible values as value
         * @throws RulesUtilsException         */
                public static Dictionary<String, ArrayList<String>> getLikeXorDict(
                                String procName, ArrayList<String> objList, boolean xorFlag) throws RulesUtilsException {
                        
                        Dictionary<String, ArrayList<String>> xorDict = new Hashtable<String, ArrayList<String>>();
            if(objList == null || objList.size() < 2){
                throw new RulesUtilsException("RulesUtils: Not enough objecs sent to xor function at "+procName);
        }
        //proc instantiations
        for (int i=0; i<SMVCreator.K;i++){
                    String linkName = (xorFlag)? "ev_xor_" : "ev_or_";
                linkName+= procName+"_"+i+"_";
                ArrayList<String> enumer = new ArrayList<String>();
                fillUpDictRegular(xorDict,linkName,enumer,objList);
                
        }
        return xorDict;
        }
                //TODO: this is not javadoc!!!
                /*the same as fillUpDict, but instead of string names of objects return this objects instances
                 * ass as arraList<String>*/
       
       
       
                
                /**
                 * This is a recursive method, which fills the dictionary with all current instantiations
                 * @param xorDict
                 * @param linkName
                 * @param enumer
                 * @param objs
                 */         
       private static void fillUpDictRegular(
                                Dictionary<String, ArrayList<String>> xorDict, String linkName,
                                ArrayList<String> enumer, ArrayList<String> objs) {
            //finished taking object to this variable, updating dictionary
            if(objs.isEmpty()){
                            xorDict.put(linkName.substring(0,linkName.length()-1), 
                                        enumer);
                            return;
                    }
            @SuppressWarnings("unchecked")
                    ArrayList<String> objsclone = (ArrayList<String>)objs.clone();
                    String currObj = objsclone.remove(0);
                    for (int i=0; i < SMVCreator.K; i++){
                            @SuppressWarnings("unchecked")
                            ArrayList<String > enumerclone = (ArrayList<String>)enumer.clone();
                            String linkNameclone = linkName + currObj + "_"+i+"_";
                            enumerclone.add(""+i);
                            fillUpDictRegular(xorDict, linkNameclone, enumerclone, objsclone);
                    } 
                        
                }

        
                
        /**
         * This is a recursive method, which fills the dictionary with all current instantiations
         * @param xorDict
         * @param linkName
         * @param enumer
         * @param objs
         * @param xorFlag
         */
        private static void fillUpDict(Dictionary<String, String> xorDict,
                                String linkName, ArrayList<String> enumer, ArrayList<String> objs, boolean xorFlag) {
                //finished taking object to this variable, updating dictionary
                if(objs.isEmpty()){
                                xorDict.put(linkName.substring(0,linkName.length()-1), makeStringOfValues(enumer,xorFlag));
                                return;
                        }
                @SuppressWarnings("unchecked")
                        ArrayList<String> objsclone = (ArrayList<String>)objs.clone();
                        String currObj = objsclone.remove(0);
                        for (int i=0; i < SMVCreator.K; i++){
                                @SuppressWarnings("unchecked")
                                ArrayList<String > enumerclone = (ArrayList<String>)enumer.clone();
                                String linkNameclone = linkName + currObj + "_"+i+"_";
                                enumerclone.add(currObj+"_"+i);
                                fillUpDict(xorDict, linkNameclone, enumerclone, objsclone, xorFlag);
                        }               
         }
        
        /**
         * 
         * @param eventName the event or/xor name
         * @param procName the name of the process (without the instantiation)
         * @param xorFlag true for xor, false for or
         * @return The process full name (name+instance), taken from the event name.
         */
        public static String getProcFullName(String eventName, String procName, boolean xorFlag) {
                int procLength = procName.length() +2;
                if (xorFlag) {
                        return eventName.substring(7, 7+procLength);
                }
                else {
                        return eventName.substring(6, 6+procLength);
                }
        }
        

        /** 
         * This function creates the value list of xor and or
         * @param enumer
         * @param xorFlag
         * @return
         */
         private static String makeStringOfValues(ArrayList<String> enumer,
                                					boolean xorFlag) 
         {
                        String values ="";
                        if(xorFlag){//it's an "or"
                                values+= "false,";
                                for (String obj : enumer) {
                                        values+= obj+"_,";
                                }
                        }
                        else{
                                values = "false,"+getOrValues(values,enumer);
                        }
                        int vallen = values.length();
                        if(vallen == 0) return values;
                        values = values.substring(0, vallen-1);
                        return values;
         }
                
                /**
                 * This function return a string of all possible combinations of object names
                 * @param enumer
                 * @param str
                 * @return
                 */
                private static String getOrValues(String str,ArrayList<String> enumer) {
                        if (enumer.size() == 0) return null;
                        String currInstance =  enumer.remove(0);
                        if (enumer.size() == 0){
                                //returning the string without the last "_"
                                return str+currInstance+"_"+","+str;
                        /*      int len = str.length()-1;
                                if(len < 0) return str;
                                return str.substring(0,len);*/
                        }
                        //returning all values that contains currInsance and all that doesn't
                        @SuppressWarnings("unchecked")
                        ArrayList<String> enumer2 = (ArrayList<String>)enumer.clone();
                        return getOrValues(str+currInstance+"_",enumer)+","+getOrValues(str,enumer2);
                        
                }
                
                /**
                 * given a list of objects with their instances, the method returns a list of strings
                 * which include all the possible combinations on the objects, if numObjsToChooseFrom
                 * are existing objects, and the rest are non-existent objects.
                 * @param objectsWithInstances
                 * @param numObjsToChooseFrom
                 * @return
                 */
                public static Dictionary<String, String> getCombinationsByIndex(ArrayList<String> objectsWithInstances, 
                		int numObjsToChooseFrom, boolean xorFlag) 
                {
                	Dictionary<String, String> results = new Hashtable<String, String>();
                	ArrayList<String> temp = new ArrayList<String>();


                	String result = "";
                	String forLottery = "";
                	ArrayList<ArrayList<String>> subsets = getSubsets(objectsWithInstances);
                	for (ArrayList<String> list : subsets) {
                		forLottery = "false";
                		if ( (list.size() == numObjsToChooseFrom) && (list.size() > 0) ) {
                			for (String obj : list) {
                				temp.add(obj + " = notExist");
                				if (xorFlag) {
                    				forLottery += "," + obj + "_";
                				}
                			}
                			for (String obj : objectsWithInstances) {
                				if (! list.contains(obj)) {
                					temp.add(obj + " = exist");
                				}
                			}
                		}
                		result = "";
                		for (String obj : temp) {
                			result = SmvOp.and(obj , result);
                		}
                		if (! xorFlag) {
                			forLottery += createOrCombinations(list);
                		}
                		if (! result.equals("")) {
                			results.put(result, forLottery);
                		}
                		temp.removeAll(temp);
                	}
                	return results;
                	
                }
                
                /**
                 * 
                 * @param objs a list of objects with their instances
                 * @return
                 */
                private static String createOrCombinations(ArrayList<String> objs) {
                	String result = "";
                	String temp = "";
                	ArrayList<ArrayList<String>> subSets = getSubsets(objs);
                	for (ArrayList<String> s : subSets) {
                		if (s.size() > 0) {
                			for (String curr : s) {
                				temp += curr + "_";
                			}
                		}
                		if (! temp.equals("")) {
                			result += "," + temp;
                		}
                		temp = "";
                	}
                	return result;
                }
        
}